Definitions | type List, t T, s = t, Type, x:AB(x), x:A. B(x), Linorder(T;x,y.R(x;y)), b, sorted-by(R;L), no_repeats(T;l), P Q, f(a), , x.A(x), x,y. t(x;y), P Q, , insert-by(eq;r;x;l), P & Q, x:A B(x), P Q, [car / cdr], S T, |g|, A, #$n, {x:A| B(x)} , l[i], ||as||, [], , , A B, {i..j}, a < b, (x l), Void, False, ff, b, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, , x f y, =, a < b, =, =, [d], p q, p q, p q, tt, Unit, left + right, if b then t else f fi , A List, xL. P(x), P Q, <a, b>, AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), Connex(T;x,y.R(x;y)), Order(T;x,y.R(x;y)), case b of inl(x) => s(x) | inr(y) => t(y) |